Nuprl Lemma : es_realizer_ind_wf 11,40
X:Type{j}, x1:es_realizer{i:l}, none:X, plus:(es_realizer{i:l}es_realizer{i:l}XXX),
init:(Id(T:Type{i}Id(T + (rationalsT))X)), frame:(IdType{i}Id(Knd List)X),
sframe:(IdLnkId(Knd List)X),
effect:(Id(ds:fpf(Id; x.Type{i})Knd
effect:(Id((T:Type{i}x:Id((decl-state(ds)Tdecl-type{i:l}
effect:(Id((T:Type{i}x:Id((decl-state(ds)Tdecl-type(ds; x)) + (decl-state(ds)T
effect:(Id((T:Type{i}x:Id(rationalsdecl-type{i:l}
effect:(Id((T:Type{i}x:Id(rationalsdecl-type(ds; x)))
effect:(Id((X))),
sends:(ds:fpf(Id; x.Type{i})Knd
sends:((T:Type{i}IdLnk(dt:fpf(Id; x.Type{i})((tg:Id
sends:((T:Type{i}IdLnk(dt:fpf(Id; x.Type{i})( (decl-state(ds)T(decl-type{i:l}
sends:((T:Type{i}IdLnk(dt:fpf(Id; x.Type{i})( (decl-state(ds)T(decl-type(dt; tg
sends:((T:Type{i}IdLnk(dt:fpf(Id; x.Type{i})( (decl-state(ds)T(decl-type() List))) List)
sends:((T:Type{i}IdLnk(X))),
pre:(Id(ds:fpf(Id; x.Type{i})Idfinite-prob-space(decl-state(ds))X)),
aframe:(IdKnd(Id List)X), bframe:(IdKnd(IdLnk List)X), rframe:(IdId(Knd List)X).
es_realizer_ind(x1;
es_realizer_ind(none;
es_realizer_ind(left,right,rec1,rec2.plus(left,right,rec1,rec2);
es_realizer_ind(loc,T,x,v.init(loc,T,x,v);
es_realizer_ind(loc,T,x,L.frame(loc,T,x,L);
es_realizer_ind(lnk,tag,L.sframe(lnk,tag,L);
es_realizer_ind(loc,ds,knd,T,x,f.effect(loc,ds,knd,T,x,f);
es_realizer_ind(ds,knd,T,l,dt,g.sends(ds,knd,T,l,dt,g);
es_realizer_ind(loc,ds,a,p,P.pre(loc,ds,a,p,P);
es_realizer_ind(loc,k,L.aframe(loc,k,L);
es_realizer_ind(loc,k,L.bframe(loc,k,L);
es_realizer_ind(loc,x,L.rframe(loc,x,L))
 X 
latex

Definitionst.2, t.1, Y, x. t(x), x(s1,s2,s3,s4,s5), x(a,b,c,d,e,f), x(s1,s2,s3), x(s1,s2,s3,s4), es realizer ind, t  T, es_realizer{i:l}, x:A. B(x), x(s)
Lemmases realizer wf, bool wf, finite-prob-space wf, decl-type wf, decl-state wf, fpf wf, IdLnk wf, Knd wf, rationals wf, Id wf, unit wf

origin